/*
 *   This program is free software: you can redistribute it and/or modify
 *   it under the terms of the GNU General Public License as published by
 *   the Free Software Foundation, either version 3 of the License, or
 *   (at your option) any later version.
 *
 *   This program is distributed in the hope that it will be useful,
 *   but WITHOUT ANY WARRANTY; without even the implied warranty of
 *   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 *   GNU General Public License for more details.
 *
 *   You should have received a copy of the GNU General Public License
 *   along with this program.  If not, see <http://www.gnu.org/licenses/>.
 */

/*
 *    Queue.java
 *    Copyright (C) 1999-2012 University of Waikato, Hamilton, New Zealand
 *
 *    Modified March-May 2004 by Mark Utting to add JML specs
 *    (this was done as the example solution of an assignment for a
 *     software engineering course, so the specifications are more precise
 *     and complete than one would normally do).
 *    Passed a static analysis using ESC/Java-2.0a6 with no warnings.
 */

package weka.core;

import java.io.Serializable;

/**
 * Class representing a FIFO queue.
 *
 * @author Len Trigg (trigg@cs.waikato.ac.nz)
 * @version $Revision$
 */
public class Queue extends Object implements Serializable {

    /** for serialization */
    private static final long serialVersionUID = -1141282001146389780L;

    /**
     * Represents one node in the queue.
     */
    protected class QueueNode implements Serializable {

        /** for serialization */
        private static final long serialVersionUID = -5119358279412097455L;

        /** The next node in the queue */
        protected /* @ spec_public @ */ QueueNode m_Next;

        /**
         * The nodes contents
         */
        protected /* @ non_null spec_public @ */ Object m_Contents;

        /**
         * Creates a queue node with the given contents
         */
        // @ requires contents != null;
        // @ assignable m_Contents, m_Next;
        // @ ensures m_Contents == contents;
        // @ ensures m_Next == null;
        public QueueNode(Object contents) {
            m_Contents = contents;
            next(null);
        }

        /**
         * Sets the next node in the queue, and returns it.
         */
        // @ requires next != this ;
        // @ assignable m_Next;
        // @ ensures m_Next==next && \result==next;
        public QueueNode next(QueueNode next) {
            return m_Next = next;
        } // @ nowarn Invariant; // Because it stupidly checks the Queue invariant!

        /**
         * Gets the next node in the queue.
         */
        // @ ensures \result == m_Next;
        public /* @ pure @ */ QueueNode next() {
            return m_Next;
        }

        /**
         * Sets the contents of the node.
         */
        // @ requires contents != null;
        // @ assignable m_Contents;
        // @ ensures m_Contents == contents && \result == contents;
        public Object contents(Object contents) {
            return m_Contents = contents;
        }

        /**
         * Returns the contents in the node.
         */
        // @ ensures \result == m_Contents;
        public /* @ pure @ */ Object contents() {
            return m_Contents;
        }

    }

    /** Store a reference to the head of the queue */
    protected /* @ spec_public @ */ QueueNode m_Head = null;

    /** Store a reference to the tail of the queue */
    protected /* @ spec_public @ */ QueueNode m_Tail = null;

    /** Store the c m_Tail.m_Nexturrent number of elements in the queue */
    protected /* @ spec_public @ */ int m_Size = 0;

    // @ public invariant m_Head == null <==> m_Tail == null;
    // @public invariant m_Tail != null ==> m_Tail.m_Next == null;
    // @ public invariant m_Size >= 0;
    // @ public invariant m_Size == 0 <==> m_Head == null;
    // @ public invariant m_Size == 1 <==> m_Head != null && m_Head == m_Tail;
    // @ public invariant m_Size > 1 ==> m_Head != m_Tail;
    // @ public invariant m_Size > 1 <== m_Head != m_Tail;

    /**
     * Removes all objects from the queue m_Tail.m_Next.
     */
    // @ assignable m_Size, m_Head, m_Tail;
    // @ ensures m_Size == 0;
    // @ ensures m_Head == null;
    // @ ensures m_Tail == null;
    public final synchronized void removeAllElements() {
        m_Size = 0;
        m_Head = null;
        m_Tail = null;
    }

    /**
     * Appends an object to the back of the queue.
     *
     * @param item the object to be appended
     * @return the object appended
     */
    // @ requires item != null;
    // @ assignable m_Head, m_Tail, m_Tail.m_Next, m_Head.m_Next, m_Size;
    // @ ensures m_Head != null;
    // @ ensures m_Tail != \old(m_Tail);
    // @ ensures m_Size == \old(m_Size) + 1;
    // @ ensures \old(m_Size) == 0 ==> m_Head == m_Tail;
    // @ ensures \old(m_Size) != 0 ==> m_Head == \old(m_Head);
    // @ ensures m_Tail.contents() == \old(item);
    // @ ensures \result == item;
    public synchronized Object push(Object item) {
        QueueNode newNode = new QueueNode(item);

        if (m_Head == null) {
            m_Head = m_Tail = newNode;
        } else {
            m_Tail = m_Tail.next(newNode);
        }
        m_Size++;
        return item;
    }

    /**
     * Pops an object from the front of the queue.
     *
     * @return the object at the front of the queue
     * @exception RuntimeException if the queue is empty
     */
    // @ assignable m_Head, m_Tail, m_Size;
    // @ ensures m_Size == \old(m_Size) - 1;
    // @ ensures m_Head == \old(m_Head.m_Next);
    // @ ensures m_Head != null ==> m_Tail == \old(m_Tail);
    // @ ensures \result == \old(m_Head.m_Contents);
    // @ signals (RuntimeException) \old(m_Head) == null;
    public synchronized Object pop() throws RuntimeException // REDUNDANT, BUT ESCJAVA REQUIRES THIS
    {
        if (m_Head == null) {
            throw new RuntimeException("Queue is empty");
        }
        Object retval = m_Head.contents();
        m_Size--;
        m_Head = m_Head.next();
        // Here we need to either tell ESC/Java some facts about
        // the contents of the list after popping off the head,
        // or turn off the 'invariant' warnings.
        //
        // @ assume m_Size == 0 <==> m_Head == null;
        // @ assume m_Size == 1 <==> m_Head == m_Tail;
        if (m_Head == null) {
            m_Tail = null;
        }
        return retval;
    }

    /**
     * Gets object from the front of the queue.
     *
     * @return the object at the front of the queue
     * @exception RuntimeException if the queue is empty
     */
    // @ ensures \result == \old(m_Head.m_Contents);
    // @ signals (RuntimeException) \old(m_Head) == null;
    public /* @ pure @ */ synchronized Object peek() throws RuntimeException {
        if (m_Head == null) {
            throw new RuntimeException("Queue is empty");
        }
        return m_Head.contents();
    }

    /**
     * Checks if queue is empty.
     * 
     * @return true if queue is empty
     */
    // @ ensures \result <==> m_Head == null;
    public /* @ pure @ */ boolean empty() {
        return m_Head == null;
    }

    /**
     * Gets queue's size.
     *
     * @return size of queue
     */
    // @ ensures \result == m_Size;
    public /* @ pure @ */ int size() {
        return m_Size;
    }

    /**
     * Produces textual description of queue.
     *
     * @return textual description of queue
     */
    // @ also
    // @ ensures \result != null;
    // @ ensures (* \result == textual description of the queue *);
    public /* @ pure @ */ String toString() {

        String retval = "Queue Contents " + m_Size + " elements\n";
        QueueNode current = m_Head;
        if (current == null) {
            return retval + "Empty\n";
        } else {
            while (current != null) {
                retval += current.contents().toString() + "\n"; // @nowarn Modifies;
                current = current.next();
            }
        }
        return retval;
    } // @ nowarn Post;

    /**
     * Main method for testing this class.
     *
     * @param argv a set of strings that are pushed on a test queue
     */
    // @ requires argv.length >= 0;
    // @ requires argv != null;
    // @ requires (\forall int i; 0 <= i && i < argv.length; argv[i] != null);
    public static void main(String[] argv) {

        try {
            Queue queue = new Queue();
            for (int i = 0; i < argv.length; i++) {
                queue.push(argv[i]);
            }
            System.out.println("After pushing command line arguments");
            System.out.println(queue.toString());
            while (!queue.empty()) {
                System.out.println("Pop: " + queue.pop().toString());
            }
            // try one more pop, to make sure we get an exception
            try {
                queue.pop();
                System.out.println("ERROR: pop did not throw exception!");
            } catch (RuntimeException ex) {
                System.out.println("Pop on empty queue correctly gave exception.");
            }
        } catch (Exception ex) {
            System.out.println(ex.getMessage());
        }
    }
}
